DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2019.20

Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL

Authors: Maximilian P. L. Haslbeck and Peter Lammich

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract

Separation Logic with Time Credits is a well established method to formally verify the correctness and run-time of algorithms, which has been applied to various medium-sized use-cases. Refinement is a technique in program verification that makes software projects of larger scale manageable. Combining these two techniques for the first time, we present a methodology for verifying the functional correctness and the run-time analysis of algorithms in a modular way. We use it to verify Kruskal’s minimum spanning tree algorithm and the Edmonds - Karp algorithm for network flow. An adaptation of the Isabelle Refinement Framework [Lammich and Tuerk, 2012] enables us to specify the functional result and the run-time behaviour of abstract algorithms which can be refined to more concrete algorithms. From these, executable imperative code can be synthesized by an extension of the Sepref tool [Lammich, 2015], preserving correctness and the run-time bounds of the abstract algorithm.

Cite as

Maximilian P. L. Haslbeck and Peter Lammich. Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{haslbeck_et_al:LIPIcs.ITP.2019.20,
  author =	{Haslbeck, Maximilian P. L. and Lammich, Peter},
  title =	{{Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.20},
  URN =		{urn:nbn:de:0030-drops-110754},
  doi =		{10.4230/LIPIcs.ITP.2019.20},
  annote =	{Keywords: Isabelle, Time Complexity Analysis, Separation Logic, Program Verification, Refinement, Run Time, Algorithms}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2016.49

Verified Analysis of List Update Algorithms

Authors: Maximilian P. L. Haslbeck and Tobias Nipkow

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract

This paper presents a machine-verified analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The analysis is verified with help of the theorem prover Isabelle; some low-level proofs could be automated.

Cite as

Maximilian P. L. Haslbeck and Tobias Nipkow. Verified Analysis of List Update Algorithms. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{haslbeck_et_al:LIPIcs.FSTTCS.2016.49,
  author =	{Haslbeck, Maximilian P. L. and Nipkow, Tobias},
  title =	{{Verified Analysis of List Update Algorithms}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{49:1--49:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.49},
  URN =		{urn:nbn:de:0030-drops-68849},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.49},
  annote =	{Keywords: Program Verification, Algorithm Analysis, Online Algorithms}
}

Search Results

Documents authored by Haslbeck, Maximilian P. L.

Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL

Abstract

Cite as

Verified Analysis of List Update Algorithms

Abstract

Cite as

Thanks for your feedback!

Could not send message